import unittest

from z3 import *


class TestSolveFunction(unittest.TestCase):
    def test_function(self):
        x = Int('x')
        y = Int('y')
        f = Function('f', IntSort(), IntSort())
        solve(f(f(x)) == x, f(x) == y, x != y)
